package com.googlecode.kipler.satisfiability.completion.rule.individual;

import java.util.Iterator;

import com.googlecode.kipler.container.dl.ABox;
import com.googlecode.kipler.container.dl.BasicWcsInterpolationData;
import com.googlecode.kipler.container.dl.ConceptCategory;
import com.googlecode.kipler.container.dl.LabelManager;
import com.googlecode.kipler.container.dl.WcsData;
import com.googlecode.kipler.satisfiability.blocking.abox.ABoxBlockingStrategy;
import com.googlecode.kipler.satisfiability.completion.rule.individual.uniformnotation.AlphaConcept;
import com.googlecode.kipler.satisfiability.reasoner.UnsatisfiableException;
import com.googlecode.kipler.syntax.concept.Concept;
import com.googlecode.kipler.syntax.formula.ConceptAssertion;

public class AlphaConceptRule extends ABoxRule {

	private ABox aBox;

	private boolean applied;

	private ABoxBlockingStrategy blocking;

	private ConceptCategory category;

	private AlphaConcept alpha;

	private String ruleName;

	public AlphaConceptRule(ABoxBlockingStrategy blocking,
			ConceptCategory category, AlphaConcept alpha, String ruleName) {
		setBlocking(blocking);
		this.category = category;
		this.alpha = alpha;
		this.ruleName = ruleName;
	}

	public ABoxBlockingStrategy getBlocking() {
		return blocking;
	}

	public void setBlocking(ABoxBlockingStrategy blocking) {
		this.blocking = blocking;
	}

	public void apply() throws UnsatisfiableException {
		applied = false;
		aBox = getWorld().getABox();
		if (!getBlocking().isIndirectlyBlocked(aBox, getIndividual().getName())) {
			for (Iterator<Concept> i = getIndividual()
					.conceptIterator(category); i.hasNext();) {
				Concept concept = i.next();
				decomposeAlphaConcept(concept);
			}
		}
	}

	private void decomposeAlphaConcept(Concept concept)
			throws UnsatisfiableException {
		alpha.setAlpha(concept);
		if (alpha.isValid()) {
			ConceptAssertion lhsAssert = new ConceptAssertion(
					alpha.getAlpha1(), getIndividual().getName());
			ConceptAssertion rhsAssert = new ConceptAssertion(
					alpha.getAlpha2(), getIndividual().getName());
			ConceptAssertion condition = new ConceptAssertion(concept,
					getIndividual().getName());
			WcsData wcsData = getWcs().getData();
			if (!aBox.contains(lhsAssert)) {
				applied = true;
				wcsData.getLogger().info(
						"WCS " + getWcs().getId() + " " + ruleName
								+ ": Adding " + lhsAssert);
				wcsData.getDependencyManager().move(lhsAssert, condition);

				if (getWcs().getReasoner().getProfile()
						.isInterpolationEnabled()) {
					LabelManager labelMan = ((BasicWcsInterpolationData) getWcs()
							.getData()).getLabelManager();
					labelMan.copyLabel(condition, lhsAssert);
				}

				aBox.add(lhsAssert);
				decomposeAlphaConcept(lhsAssert.getConcept());
			}
			if (!aBox.contains(rhsAssert)) {
				applied = true;
				wcsData.getLogger().info(
						"WCS " + getWcs().getId() + " " + ruleName
								+ ": Adding " + rhsAssert);
				wcsData.getDependencyManager()
						.move(
								rhsAssert,
								new ConceptAssertion(concept, getIndividual()
										.getName()));

				if (getWcs().getReasoner().getProfile()
						.isInterpolationEnabled()) {
					LabelManager labelMan = ((BasicWcsInterpolationData) getWcs()
							.getData()).getLabelManager();
					labelMan.copyLabel(condition, rhsAssert);
				}

				aBox.add(rhsAssert);
				decomposeAlphaConcept(rhsAssert.getConcept());
			}
		}
	}

	@Override
	public boolean isApplied() {
		return applied;
	}

}
